COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	david[w85,jmc]		Notes for David Chudnovsky
C00006 ENDMK
C⊗;
david[w85,jmc]		Notes for David Chudnovsky

David wants some notes to attract mathematicians to his conference.

	Computers can compute with symbolic expressions as well as
with numbers, and this was recognized early.  For example, programs
for symbolic differentiation and integration were first written in
the 1950s and 1960s.  However, the early programs were useful
mainly as demonstrations, because the computers, the programming
techniques and the understanding by mathematicians of the possibilities
were all lacking.

	Now the situation is quite different.  Computers with the
necessary large memories and high speeds are available.  Programming
languages like Lisp oriented to symbolic computation are wide
use.  Mathematicians, especially younger ones, have greater
familiarity with the possibilities.  Besides the symbolic programming
languages themselves, there are systems such as Macsyma, Reduce and
SMP designed specifically for interactive symbolic computation.  These
systems include algorithms for algebraic simplification, operations
with polynomials like gcd and factoring, differentiation, integration,
and other operations on integrals and series.  Many specialized
programs exist.  These programs exist both on ``main frame'' computers
accessed from terminals and on individual work stations.  Some versions
even exist on personal computers which are less expensive than
the work stations.

	Mathematically significant symbolic computations have been
done and will be discussed in the lectures and demonstrated at the
conference.  1986 seems like a good year for the use of computers
for symbolic computation by mathematicians to begin a rapid expansion.

	The use of computers for theorem proving is another area
where computer work began early, but is only now reaching the point
where it can be of actual assistance to mathematicians.  In fact
theorem proving is still considerably behind algebraic computation
in its state of usefulness.  However, we are getting the first
examples where interactive theorem provers can be made to accept
significant theorems with the same order of magnitude of work as
is required to put the proofs on paper and often considerable
gain in clarity and certainty.

	We sight Shankar's new proof of the Church-Rosser theorem
as an example where the use of a computer has helped produce a correct
understandable and short proof.  Of course, there was also a new
mathematical idea.